A:Type, B:(AType), eq1,eq2:EqDecider(A), f:fpf(A; a.B(a)), x:A.
fpf-dom(eq1; x; f) = fpf-dom(eq2; x; f)   

latex

Definitions	x:A. B(x), x(s), fpf-dom(eq; x; f), t.1, t  T, P  Q, prop{i:l}, x. t(x), fpf(A; a.B(a)), , Unit, P  Q, P  Q, A, False, , tt, ff
Lemmas	deq-member wf, bool wf, iff transitivity, assert wf, l member wf, eqtt to assert, assert-deq-member, btrue wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, bfalse wf, fpf wf, deq wf